(DEFPROP UPDATE 
 (LAMBDA(E)
  (PROG (USINGFL USING
 		 CHAN1
 		 ELOC
 		 CHAN
 		 AUTO
 		 DL1
 		 RF
 		 XYZ
 		 XYZ1
 		 CMD
 		 LOCFLG
 		 Z
 		 Z1
 		 Z2
 		 INCT
 		 Z3
 		 Z1R
 		 Z2R
 		 N1
 		 R
 		 N
 		 NAME
 		 NAMELIST
 		 ZZ)
	(SETQ CHAN (OUTC NIL NIL))
	(SETQ AXNO (QUOTE INSERT))
	(SETQ FNNAM (QUOTE EDI))
	(SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
	(SETQ N1 (LAST NAMELIST))
	(SETQ INCT (INC NIL))
   U9   (SETQ ELOC E)
	(SETQ N 1)
   U3   (UP1A (CAR ELOC) N)
   U3A  (TERPRI)
   U3AA (SETQ CMD (READ))
	(COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
   U3B  (COND ((NOT (ATOM CMD)) (GO UER2)))
   U3C  (SETQ CMD (EXPLODE CMD))
	(COND ((EQ (LENGTH CMD) 1) (GO UER1))
	      ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
   UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
	(GO U3A)
   UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
	(GO U3A)
   UDI1 (SETQ Z1 (UPGETL E NAMELIST))
	(COND ((NULL Z1) (GO U3A)))
	(CLAUSES Z1)
	(GO U3A)
   USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
	(SETQ Z NAMELIST)
   USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
	(SETQ Z (CDR Z))
	(COND (Z (GO USY2)))
	(GO U3A)
   UFL2 (SETQ Z (QUOTE U))
	(GO UFL4)
   UFL3 (SETQ Z (QUOTE D))
	(GO UFL4)
   UFL1 (SETQ Z (CAR (EXPLODE (READ))))
   UFL4 (SETQ Z2 405104)
	(COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
   UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
	(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
	(UPDATESTATE (CDDR Z))
	(GO U3A)
   UDE1 (SETQ Z2 (UPGETL E NAMELIST))
	(COND ((NULL Z2) (GO U3A)))
	(EXPUNGE Z2)
	(GO U3A)
   UIN1 (SETQ NAME (READ))
	(SETQ Z2 (UPGETL E NAMELIST))
	(COND ((NULL Z2) (GO U3A)))
   UIN1A
	(COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
	(NCONC Z1 Z2)
	(GO U3A)
   USU1 (SETQ Z1 (ERRSET (GETTERMS E NAMELIST)))
	(COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
	      ((NULL (CAR Z1)) (GO U3A)))
	(SETQ Z3 NIL)
	(SETQ Z1 (CAR Z1))
   USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
	(SETQ Z1 (CDR Z1))
	(COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2 (SET3 (SETUP Z3))) (GO UIN1A)))
   UUP1 (SETQ Z2 (READ))
	(COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U8)) (T (GO UER2)))
   UDO1 (SETQ Z2 (READ))
	(COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U7)) (T (GO UER2)))
   UAN1 (SETQ Z2 (UPGETL E NAMELIST))
   UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
	(SETQ Z2 (CDR Z2))
	(GO UAN2)
   UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
	(INC INCT)
	(OUTC CHAN NIL)
	(SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
	(SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
	(RETURN (MINIMIZE (APPEND Z1 Z)))
   USA1 (SETQ Z2 (UPGETL E NAMELIST))
	(COND (Z2 (NCONC E Z2)))
	(GO U3A)
   UPA1 (SETQ Z1 (UPGETL E NAMELIST))
	(SETQ Z2 (UPGETL E NAMELIST))
	(COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
   USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
	(COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
	(COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
	(SETQ Z3 Z1)
	(SETQ Z DDEPTH)
	(SETQ DDEPTH 22)
   USI2 (DEMOD (LIST (CAR Z3)) Z2)
	(SETQ Z3 (CDR Z3))
	(COND (Z3 (GO USI2)))
	(PRINT (QUOTE CLAUSES-ARE:))
	(CLAUSES Z1)
	(SETQ DDEPTH Z)
	(GO U3A)
   UCU1 (QUERY)
	(GO U3A)
   UDS1 (SETQ Z1 (READ))
	(COND ((NOT (ATOM Z1)) (GO UDS3)))
   UDS2 (COND
	 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
								(GO UDS2)))
   UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
	(GO U3A)
   UEO1 (OUTC CHAN1 T)
	(GO U3A)
   UUS1 (SETQ NAME (QUOTE %USING))
	(SETQ USINGFL T)
	(SETQ USING NIL)
   UUS3 (SETQ LOCFLG T)
   UUS2 (SETQ Z2 (UPGETL E NAMELIST))
	(SETQ USINGFL NIL)
	(COND ((NULL Z2) (GO U3A)))
   USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
	(COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
	      (T (RPLACA (CAR N1) NAME)
		 (RPLACD (CAR N1) Z2)
		 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
		 (SETQ N1 (CDR N1))))
	(GO U3A)
   USE1 (SETQ NAME (READ))
	(SETQ LOCFLG NIL)
	(GO UUS2)
   UCL1 (SETQ Z (READ))
   UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
	      ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
								   (GO UCL2))
	      (T (GO U3A)))
   UGO1 (SETQ Z1 (READ))
	(COND ((NOT (NUMBERP Z1)) (GO UER2)))
	(COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
	      (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
   UTR1 (SETQ AUTO NIL)
	(GO UEX2)
   UEX1 (SETQ AUTO T)
   UEX2 (SETQ NAME (QUOTE LEMMA))
	(SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
	(COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
	(SETQ Z2 (ATTEMPT (INITIALAX (CONS THEOREMNAME (APPEND XYZ USING))) NIL NIL))
	(GO AT1A)
   UST1 (STOP)
	(GO U3A)
   UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
	(ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
   U8   (COND ((EQ Z2 0) (GO U9)))
   U83  (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
	(SETQ Z2 (DIFFERENCE Z2 5))
	(SETQ ZZ 5)
   U84  (SETQ Z N)
	(SETQ Z3 (DIFFERENCE N ZZ))
	(COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
	(SETQ N Z3)
	(SETQ Z3 ELOC)
	(SETQ ELOC (DOWN N E))
	(SETQ ZZ NIL)
	(SETQ Z1 ELOC)
   U81  (COND ((EQ Z1 Z3) (GO U82)))
	(SETQ ZZ (CONS (CAR Z1) ZZ))
	(SETQ Z1 (CDR Z1))
	(GO U81)
   U82  (COND ((NULL ZZ) (GO U83)))
	(UP1A (CAR ZZ) (SUB1 Z))
	(SETQ ZZ (CDR ZZ))
	(SETQ Z (SUB1 Z))
	(GO U82)
   U7   (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
	(SETQ Z2 (PLUS Z2 N))
   U7A  (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
	(SETQ ELOC (CDR ELOC))
	(SETQ N (ADD1 N))
	(UP1A (CAR ELOC) N)
	(COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
   UPR1 (TERPRI)
	(SETQ XYZ NIL)
	(SETQ Z2 (UPGETL E NAMELIST))
	(COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
	(COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
	(SETQ AXNO THEOREMNAME)
	(SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
	(SETQ AXNO (QUOTE INSERT))
	(SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
	(COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
	(SETQ NAME (QUOTE LEMMA))
	(SETQ LOCFLG T)
	(GO USE2)
   UME1 (SETQ Z1 (UPGETL E NAMELIST))
	(SETQ Z2 (UPGETL E NAMELIST))
	(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
	(BAKSUB Z1 Z2)
	(GO U3A)
   UHE1 (PRINT MESSAGE)
	(GO U3A)
   URE1 (SETQ Z1 (UPGETL E NAMELIST))
	(SETQ Z2 (UPGETL E NAMELIST))
   U%RE1
	(SETQ RF T)
   URE1A
	(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
	(SETQ Z1R Z1)
	(SETQ Z2R Z2)
	(SETQ Z3 NIL)
	(COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
	(COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
   UR3  (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
	      ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
	(COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
	(COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
	(SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
   UR3A (SETQ Z2R (CDR Z2R))
	(COND (Z2R (GO UR3)))
	(SETQ Z1R (CDR Z1R))
	(COND (Z1R (SETQ Z2R Z2) (GO UR3)))
   UR3B (COND ((NULL Z3)
	       (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
		     (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
	      (RF (SETQ NAME (QUOTE RES)))
	      (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
	(SETQ Z2 Z3)
	(SETQ LOCFLG T)
	(GO AT2A)
   UEV1 (PRINT (QUOTE EVAL-AWAITS))
	(SETQ Z2 (ERRSET (EVAL (READ)) T))
	(COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
   UE2  (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
	(GO UEV1)
   AT1A (UPDATESTATE STRAT)
	(COND
	 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
	  (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
	  (PRINC NAME)
	  (GO U3A))
	 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
					(SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
					(SETQ AUTO NIL)
					(GO AT1A))
	 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
	(SETQ Z2 (CADR Z2))
   AT2A (SETQ N 1)
   AT2  (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
	(SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
	(PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
	(PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
	(PRIN1 NAME)
	(CLAUSES Z2)
	(GO USE2))) 
EXPR)

(DEFPROP UPDATESTATE 
 (LAMBDA (L) (PROG NIL (SETQ STRATEGY (BUILTCH (CAR L))) (SETQ EDITSTRAT (BUILTED (CDR L))) (SETQ STRAT L))) 
EXPR)